|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > cbvrex2vw | Structured version Visualization version GIF version | ||
| Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3368 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by FL, 2-Jul-2012.) Avoid ax-13 2376. (Revised by GG, 10-Jan-2024.) | 
| Ref | Expression | 
|---|---|
| cbvrex2vw.1 | ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) | 
| cbvrex2vw.2 | ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | 
| Ref | Expression | 
|---|---|
| cbvrex2vw | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | cbvrex2vw.1 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) | |
| 2 | 1 | rexbidv 3178 | . . 3 ⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜒)) | 
| 3 | 2 | cbvrexvw 3237 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) | 
| 4 | cbvrex2vw.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
| 5 | 4 | cbvrexvw 3237 | . . 3 ⊢ (∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑤 ∈ 𝐵 𝜓) | 
| 6 | 5 | rexbii 3093 | . 2 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | 
| 7 | 3, 6 | bitri 275 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∃wrex 3069 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-clel 2815 df-rex 3070 | 
| This theorem is referenced by: omeu 8624 oeeui 8641 eroveu 8853 genpv 11040 bezoutlem3 16579 bezoutlem4 16580 bezout 16581 4sqlem2 16988 vdwnn 17037 efgrelexlema 19768 dyadmax 25634 2sqlem9 27472 2sq 27475 mulsval2lem 28137 mulsunif2 28197 precsexlemcbv 28231 legov 28594 dfcgra2 28839 gsumwun 33069 pstmfval 33896 satfv0 35364 satfv0fun 35377 fmla1 35393 nn0prpwlem 36324 isbnd2 37791 hashnexinjle 42131 aks6d1c6lem3 42174 nna4b4nsq 42675 oaun3lem1 43392 limsupref 45705 fourierdlem42 46169 fourierdlem54 46180 mogoldbb 47777 | 
| Copyright terms: Public domain | W3C validator |