| 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 1871 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
| 3 | df-rex 3090 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 4 | df-rex 3090 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
| 5 | 2, 3, 4 | 3bitr4i 306 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 209 ∧ wa 400 ∃wex 1802 ∈ wcel 2145 ∃wrex 3089 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 |
| This theorem depends on definitions: df-bi 210 df-ex 1803 df-rex 3090 |
| This theorem is referenced by: rexbiia 3110 rexeqbii 3338 rexrab 3662 rexin 4205 rexdifpr 4621 rexdifsn 4757 reusv2lem4 5362 reusv2 5364 frpoind 6332 eldifsucnn 8638 frind 9710 rexuz2 12911 rexrp 13027 rexuz3 15388 infpn2 16961 efgrelexlemb 19808 cmpcov2 23504 cmpfi 23522 txkgen 23766 cubic 26968 madeval2 27980 sumdmdii 32672 extdgfialglem1 33994 bnj882 35226 bnj893 35228 heibor1 38316 eldmqsres 38799 prtlem100 39490 islmodfg 43653 iuneq1i 45663 limcrecl 46204 |
| Copyright terms: Public domain | W3C validator |