![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexbii2 | Structured version Visualization version GIF version |
Description: Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.) |
Ref | Expression |
---|---|
rexbii2.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)) |
Ref | Expression |
---|---|
rexbii2 | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexbii2.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)) | |
2 | 1 | exbii 1833 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3113 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3113 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3bitr4i 304 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∃wex 1765 ∈ wcel 2083 ∃wrex 3108 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 |
This theorem depends on definitions: df-bi 208 df-ex 1766 df-rex 3113 |
This theorem is referenced by: rexbiia 3212 rexbii 3213 rexeqbii 3289 rexrab 3628 rexin 4142 rexdifpr 4509 rexdifsn 4640 reusv2lem4 5200 reusv2 5202 wfi 6063 rexuz2 12152 rexrp 12264 rexuz3 14546 infpn2 16082 efgrelexlemb 18607 cmpcov2 21686 cmpfi 21704 txkgen 21948 cubic 25112 sumdmdii 29879 bnj882 31810 bnj893 31812 frpoind 32691 frind 32696 madeval2 32901 heibor1 34641 eldmqsres 35096 prtlem100 35547 islmodfg 39175 limcrecl 41473 |
Copyright terms: Public domain | W3C validator |