![]() |
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 1851 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∃wex 1782 ∈ wcel 2107 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-rex 3071 |
This theorem is referenced by: rexbiia 3092 rexeqbii 3315 rexrab 3655 rexin 4200 rexdifpr 4620 rexdifsn 4755 reusv2lem4 5357 reusv2 5359 frpoind 6297 wfiOLD 6306 eldifsucnn 8611 frind 9691 rexuz2 12829 rexrp 12941 rexuz3 15239 infpn2 16790 efgrelexlemb 19537 cmpcov2 22757 cmpfi 22775 txkgen 23019 cubic 26215 madeval2 27205 sumdmdii 31399 bnj882 33595 bnj893 33597 heibor1 36315 eldmqsres 36793 prtlem100 37367 islmodfg 41439 limcrecl 43956 |
Copyright terms: Public domain | W3C validator |