2exbii - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem 2exbii 1050

Description: Inference adding 2 existential quantifiers to both sides of an equivalence.

**Hypothesis**
Ref	Expression
2exbii.1

**Assertion**
Ref	Expression
2exbii

**Proof of Theorem 2exbii**
Step	Hyp	Ref	Expression
1		2exbii.1	. . 3
2	1	exbii 1049	. 2
3	2	exbii 1049	1

Colors of variables: wff set class

Syntax hints:

wb 146

wex 978

This theorem is referenced by: 3exbi 1051 cbvex4v 1320 ee4anv 1323 sbel2x 1343 2eu4 1450 2eu6 1452 rexcom 1772 reeanv 1775 opabid 2805 opabn0 2819 uniuni 2875 elxp3 3219 elvv 3223 elcnv2 3289 cnvuni 3296 coass 3504 fununi 3555 dfoprab2 3982 dmoprab 3993 rnoprab 3995 resoprab 4000 fnoprval 4008 oprabex3 4013 oprabval3 4021 oprabval6g 4023 1st2val 4085 2nd2val 4086 xpcomen 4425 xpassen 4427 zorn2lem6 4773 genpn0 5086 genpass 5092 addcompr 5103 mulcompr 5105 distrlem5pr 5111 ltresr 5238 axaddopr 5245 axmulopr 5246 replimt 6700 nvvcop 8165 5oalem7 9545

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 961 ax-4 971 ax-5o 973

This theorem depends on definitions: df-bi 147 df-an 225 df-ex 979