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 1844 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3144 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3144 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3bitr4i 305 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∃wex 1776 ∈ wcel 2110 ∃wrex 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 209 df-ex 1777 df-rex 3144 |
This theorem is referenced by: rexbiia 3246 rexbii 3247 rexeqbii 3326 rexrab 3687 rexin 4216 rexdifpr 4592 rexdifsn 4721 reusv2lem4 5294 reusv2 5296 wfi 6176 rexuz2 12293 rexrp 12404 rexuz3 14702 infpn2 16243 efgrelexlemb 18870 cmpcov2 21992 cmpfi 22010 txkgen 22254 cubic 25421 sumdmdii 30186 bnj882 32193 bnj893 32195 frpoind 33075 frind 33080 madeval2 33285 heibor1 35082 eldmqsres 35537 prtlem100 35989 islmodfg 39662 limcrecl 41902 |
Copyright terms: Public domain | W3C validator |