Theorem ralrn 7060

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Hypothesis

Ref	Expression
rexrn.1	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrn	⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem ralrn

Step	Hyp	Ref	Expression
1		fvexd 6873	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6921	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2736	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3076	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 287	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5365	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  Vcvv 3447  ran crn 5639   Fn wfn 6506  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-fv 6519

This theorem is referenced by:  ralrnmptw  7066  ralrnmpt  7068  cbvfo  7264  isoselem  7316  indexfi  9311  ordtypelem9  9479  ordtypelem10  9480  wemapwe  9650  numacn  10002  acndom  10004  rpnnen1lem3  12938  fsequb2  13941  limsuple  15444  limsupval2  15446  climsup  15636  ruclem11  16208  ruclem12  16209  prmreclem6  16892  imasaddfnlem  17491  imasvscafn  17500  cycsubgcl  19138  ghmrn  19161  ghmnsgima  19172  pgpssslw  19544  gexex  19783  dprdfcntz  19947  znf1o  21461  frlmlbs  21706  lindfrn  21730  ptcnplem  23508  kqt0lem  23623  isr0  23624  regr1lem2  23627  uzrest  23784  tmdgsum2  23983  imasf1oxmet  24263  imasf1omet  24264  bndth  24857  evth  24858  ovolficcss  25370  ovollb2lem  25389  ovolunlem1  25398  ovoliunlem1  25403  ovoliunlem2  25404  ovoliun2  25407  ovolscalem1  25414  ovolicc1  25417  voliunlem2  25452  voliunlem3  25453  ioombl1lem4  25462  uniioovol  25480  uniioombllem2  25484  uniioombllem3  25486  uniioombllem6  25489  volsup2  25506  vitalilem3  25511  mbfsup  25565  mbfinf  25566  mbflimsup  25567  itg1ge0  25587  itg1mulc  25605  itg1climres  25615  mbfi1fseqlem4  25619  itg2seq  25643  itg2monolem1  25651  itg2mono  25654  itg2i1fseq2  25657  itg2gt0  25661  itg2cnlem1  25662  itg2cn  25664  limciun  25795  plycpn  26197  hmopidmchi  32080  hmopidmpji  32081  rge0scvg  33939  mclsax  35556  mblfinlem2  37652  ismtyhmeolem  37798  nacsfix  42700  fnwe2lem2  43040  gneispace  44123  climinf  45604  liminfval2  45766