Theorem sbc2or 1454

Description: The disjunction of two equivalences for class substitution does not require a class existence hypothesis.

Assertion

Ref	Expression
sbc2or	|- (([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> A.x(x = A -> ph)))

Distinct variable group(s):   x,A

Proof of Theorem sbc2or

Step	Hyp	Ref	Expression
1		sbc5g 1450	. . 3 |- (A e. V -> ([A / x]ph <-> E.x(x = A /\ ph)))
2		orc 225	. . 3 |- (([A / x]ph <-> E.x(x = A /\ ph)) -> (([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> A.x(x = A -> ph))))
3	1, 2	syl 12	. 2 |- (A e. V -> (([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> A.x(x = A -> ph))))
4		exmid 494	. . . 4 |- (([A / x]ph <-> E.x(x = A /\ ph)) \/ -. ([A / x]ph <-> E.x(x = A /\ ph)))
5		pm5.18 497	. . . . . 6 |- (([A / x]ph <-> E.x(x = A /\ ph)) <-> -. ([A / x]ph <-> -. E.x(x = A /\ ph)))
6	5	bicon2i 194	. . . . 5 |- (([A / x]ph <-> -. E.x(x = A /\ ph)) <-> -. ([A / x]ph <-> E.x(x = A /\ ph)))
7	6	orbi2i 214	. . . 4 |- ((([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> -. E.x(x = A /\ ph))) <-> (([A / x]ph <-> E.x(x = A /\ ph)) \/ -. ([A / x]ph <-> E.x(x = A /\ ph))))
8	4, 7	mpbir 165	. . 3 |- (([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> -. E.x(x = A /\ ph)))
9		pm5.1 501	. . . . . 6 |- ((-. E.x(x = A /\ ph) /\ A.x(x = A -> ph)) -> (-. E.x(x = A /\ ph) <-> A.x(x = A -> ph)))
10		visset 1350	. . . . . . . . . 10 |- x e. V
11		eleq1 1149	. . . . . . . . . 10 |- (x = A -> (x e. V <-> A e. V))
12	10, 11	mpbii 168	. . . . . . . . 9 |- (x = A -> A e. V)
13	12	adantr 306	. . . . . . . 8 |- ((x = A /\ ph) -> A e. V)
14	13	con3i 90	. . . . . . 7 |- (-. A e. V -> -. (x = A /\ ph))
15	14	nexdv 983	. . . . . 6 |- (-. A e. V -> -. E.x(x = A /\ ph))
16	12	con3i 90	. . . . . . . 8 |- (-. A e. V -> -. x = A)
17	16	pm2.21d 74	. . . . . . 7 |- (-. A e. V -> (x = A -> ph))
18	17	19.21aiv 943	. . . . . 6 |- (-. A e. V -> A.x(x = A -> ph))
19	9, 15, 18	sylanc 361	. . . . 5 |- (-. A e. V -> (-. E.x(x = A /\ ph) <-> A.x(x = A -> ph)))
20	19	bibi2d 470	. . . 4 |- (-. A e. V -> (([A / x]ph <-> -. E.x(x = A /\ ph)) <-> ([A / x]ph <-> A.x(x = A -> ph))))
21	20	orbi2d 466	. . 3 |- (-. A e. V -> ((([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> -. E.x(x = A /\ ph))) <-> (([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> A.x(x = A -> ph)))))
22	8, 21	mpbii 168	. 2 |- (-. A e. V -> (([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> A.x(x = A -> ph))))
23	3, 22	pm2.61i 110	1 |- (([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> A.x(x = A -> ph)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195   /\ wa 196  A.wal 672  E.wex 678   = wceq 1091   e. wcel 1092  Vcvv 1348  [wsbc 1440

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-sbc 1441

metamath.org